Inference at * 1 
Iof proof for Lemma assert of eq bool:



1. p : 
2. q : 
  (p =b q)  (p = q) 

latex

 by Unfold `eq_bool` 0 

latex

 1: 

 1:   (((p  q) ((p)  (q))))  (p = q)
 .

Definitions

p =b q